COMMENT ⊗   VALID 00007 PAGES
C REC  PAGE   DESCRIPTION
C00001 00001
C00002 00002	.require "memo.pub[let,jmc]" source
C00013 00003	#. Derived functions
C00015 00004	#. Occurrences of an atom in an S-expression.
C00016 00005	#. Improving LCOM4
C00017 00006	# Pattern matching and substitution
C00019 00007	#. Simplifying expressions
C00020 ENDMK
C⊗;
.require "memo.pub[let,jmc]" source
.turn on "→"
CS206∂(30)FINAL EXAMINATION→FALL 1981
.turn off "→"

	This examination is open book and notes.
Write LISP functions or predicates and make proofs
 as follows except where something else is
requested.  Either notation may be used.
Be sure to indicate in an emphatic way the logical sentences indicating
what is to be proved and the %AF%*'s of any inductions that need to be
made.  You may assume that your functions are total but will be
suitably penalized if they aren't.

	The examination is a "take home" and is due at 1981 December 17
Thursday 7pm in Room 353 Margaret Jacks Hall.  It may also be left
earlier with Mrs. Larson in Room 358 Margaret Jacks Hall.
.item←0

#. Derived functions

	Certain properties of LISP functions are expressed by related
functions called derived functions.  For example, consider

%2flatten x ← qif qat x qthen <x> qelse flatten qa x * flatten qd x%1.

Let %2cflatten x%1 be the number of times LISP executes ⊗cons in
evaluating %2flatten x%1.  Clearly ⊗cflatten satisfies the recursions

%2cflatten x ← qif qat x qthen 1
	qelse cflatten qa x + cflatten qd x + cappend[flatten qa x, flatten qd x]%1,

where ⊗cappend[u,v] is the number of conses done in computing %2u*v%1
and satisfies

%2cappend[u,v] ← qif qn u then 0 qelse 1 + cappend[qd u, v]%1.

	Our other way of flattening a list involves

%2flat[x,u] ← qif qat x qthen x.u qelse flat[qa x, flat[qd x, u]]%1.

Let ⊗cflat[x,u] be the number of %2cons%1es done in computing %2flat[x,u]%1.

	a. Write the recursion for %2cflat[x,u]%1.

	b. Prove %2cflat[x,u] ≤ cflatten x%1.

#. Occurrences of an atom in an S-expression.

	Define

%2occurs[x,y] ← qif qat y qthen x = y qelse occurs[x, qa y] ∨ occurs[x, qd y]%1.

and

%2occurrences[x,y,u] ← qif qat y qthen [qif x = y qthen x.u qelse u] qelse occurrences[x, qa y, occurrences[x,qd y, u]]%1.

%1Prove

	%2∀x.atom x ⊃ ∀y.occurs[x,y] ≡ member[x, occurrences[x,y,qnil]]%1.

#. Improving LCOM4

	Page 172 of the text gives code compiled by LCOM4 for the function
%2drop%1 defined slightly earlier in the text.

a. Why is the second executed instruction (MOVE 1 0 P) unnecessary?

b. Describe modifications to LCOM4 that would (preserving correctness)
avoid generating this instruction.

# Pattern matching and substitution

	%2sublis[pattern, alist]%1 is the result of making the
substitutions described in ⊗alist in ⊗pattern.  Thus

%2sublis%1[(PLUS X (TIMES X Y) A), ((X.A) (Y.(PLUS X Y)))] 
		= (PLUS A (TIMES A (PLUS X Y)) A)

%2match[pattern,expression,alist]%1 attempts to match ⊗pattern against
⊗expression to produce and extension of ⊗alist such that substituting
in the pattern according to the result will lead give back %2expression%1.
If the match is unsuccessful, the value is the atom NO.  It is assumed
that a predicate  ⊗isvar  applicable to atoms is available that distinguishes
variables from other atoms.  Assuming that ⊗X and ⊗Y are variables, we have

%2match%1[(PLUS X Y), (PLUS A (TIMES B C)),qnil] = ((X.A) (Y TIMES B C)),

and

%2match%1[(PLUS X Y), (PLUS A (TIMES B C)),((X.B))] = NO.

a. Write recursive programs for ⊗sublis and ⊗match. 

b. Write accurately the sentence that expresses the fact that
⊗sublis and ⊗match are partial inverses.

c. Prove the sentence of part b.
#. Simplifying expressions

	Write a program for simplifying expressions formed from
sums and products of arbitrary length that

(1) appropriately eliminates sums and products with zero or one terms.

(2) drops summands that are 0 and factors that are 1

(3) drops products that have a term that is 0

b. Prove that for all values of the variables, the
simplified expression has the same value as the original expression.

c. Define an appropriate complexity and prove that the result of
simplification is not more complex than the input.